$\vdash$  $\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $d$:($\forall$$x$:$A$. Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($x$,$n$))))). mu'($P$) $\in$ $A$$\rightarrow$($\mathbb{N}$ + Top)